\begin{tabbing}
st{-}lookup(${\it tab}$;$x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=let $K$,$p$,$f$ = ${\it tab}$ in \+
\\[0ex]let $n$\= = mu($\lambda$$n$.$p$ $<$z $n$ $\vee_{b}$$K$ $\leq$z $n$ $\vee_{b}$eq\_atom1(($f$($n$)).1;$x$)) in\+
\\[0ex]if $p$ $<$z $n$ $\vee_{b}$$K$ $\leq$z $n$ then inr $\cdot$  else inl (($f$($n$)).2)  fi 
\-\-
\end{tabbing}